This seems 'too easy' but to certify things I don't think it needs to be more complex? #6513
Conversation
… be more complex?
ramsay-t
added
No Changelog Required
ramsay-t
temporarily deployed
to
github-pages
GitHub Actions
Inactive
ramsay-t
temporarily deployed
to
github-pages
GitHub Actions
Inactive
| data UCSE : Relation where | ||
| cse : {X : Set} {x : Maybe X ⊢} {x' e : X ⊢} | ||
| → Translation UCSE (x [ e ]) x' | ||
| → UCSE ((ƛ x) · e) x' |
There was a problem hiding this comment.
Well just like with float-delay, you gotta make sure that e is pure. If the implementation pulls out an effectful e, then this may be a bug in the implementation.
... but unfortunately, it may not be a bug, sometimes it is fine to move impure things around for as long as that doesn't change the semantics of the program (and then there's an entirely separate discussion on whether effect ordering is important or not). For example if you have a bunch of applied lambda and all but one are pure, then it doesn't really matter in which order to execute them, since you're still going to get the single effect that you're ought to get.
So I suggest to reflect what I just said. Require e to be pure and say that this isn't the most general correct CSE, but is sufficient for now. Perhaps also add a link to this discussion.
| isUCSE? : {X : Set} {{_ : DecEq X}} → Binary.Decidable (UCSE {X}) | ||
| isUCSE? ast ast' with (isApp? (isLambda? isTerm?) isTerm?) ast | ||
| ... | no ¬match = no λ { (cse x) → ¬match (isapp (islambda (isterm _)) (isterm _)) } | ||
| ... | yes (isapp (islambda (isterm x)) (isterm e)) with isUntypedCSE? (x [ e ]) ast' |
There was a problem hiding this comment.
I think the whole approach to certification is very suboptimal. I.e. this pass and the others (not sure if all of them). So what you do here is you check that the LHS has the right shape and then you proceed with substitution and recurse. Potentially just to figure out that you didn't need to do all this work, because the terms match exactly and there was no point in all these substitutions and non-deterministic digressing into CSE, float-delay and everything else at every lambda application node.
I guess this is a fine start, but I wouldn't be surprised if it eventually turns out that all the passes need to be rewritten, because they can't handle real-world terms fast enough.
There was a problem hiding this comment.
If they are identical then that should be handled by translation? before it gets into this decision procedure.
It isn't because this one runs first in translation? because if it didn't then we might get half way down the AST before realising we need to look at some of the higher structure for the specific relation, and I'm not sure how neat the backtracking is in translation?. That is what I'd look at first...
There was a problem hiding this comment.
If they are identical then that should be handled by
translation?before it gets into this decision procedure.
Nope, translation? invokes isR? before doing anything else.
There was a problem hiding this comment.
The word "should" was important in that sentence :)
* WIP * WIP * WIP * WIP * WIP * WIP - Most of the nFD->FD proof is done but I am now wondering if the application rules need the force in them... * Some progress on the FD->pureFD proof... Not completely sure it is going in a good direction... * Made the parameters to istranslation implicit, since they are encoded in the relation anyway * WIP * WIP * WIP - with crazy variable binding issues * Add 'forall DecEq' to 'Relation' * Roman's additions. * Workign Float-Delay translation relation and decision procedure. * Missed a definition * Now uses Purity, althought that is 'stub code' at the moment. * Now with added Purity... * Remove 'Terminating' from 'translation?' --------- Co-authored-by: effectfully <[email protected]>
ramsay-t
temporarily deployed
to
github-pages
GitHub Actions
Inactive
ramsay-t
temporarily deployed
to
github-pages
GitHub Actions
Inactive
ramsay-t
temporarily deployed
to
github-pages
GitHub Actions
Inactive
ramsay-t
temporarily deployed
to
github-pages
GitHub Actions
Inactive
A straightforward Translation Relation for CSE certification. Perhaps there are some more subtle things we want to check?
Fixes #6370